es:ES, a:Atom1, e:E.
e sends a  (state when e):state@loc(e)>>a
 loc(e) >> a
  (e':E. e'  e  & e' receives a)
  (state when es-init(es;e)):state@loc(es-init(es;e))>>a 

latex

Definitions

t  T, x:A. B(x), A, P  Q, b, , Prop, False, x:AB(x), x:AB(x), P & Q, P  Q, Unit, left+right, state@i, x:A. B(x), x:T>>a, E, A & B, P  Q, Void, e  e' , P  Q, (e <loc e'), Type, AtomFree(T;x), val(e), valtype(e), isrcv(e), es-init(es;e), {T}, (state when e), A/x,y. B(x;y), 1of(t), ES, Atom$n, WellFnd{i}(A;x,y.R(x;y)), i >> a, <a,b>, SQType(T), s ~ t, e sends a, (e < e'), sender(e), Dec(P), x.A(x), x. t(x), e receives a, loc(e), pred(e), Id, s = t, first(e), b, lexpr{i}

Lemmas

es-causl-wellfnd, event system-level-subtype, event system wf, es-atom-axiom, es-le-self, decidable assert, es-pred-le, subtype rel self, es-send-atom wf, es-causl-iff, es-sender wf, es-causl wf, es-atom wf, Id wf, Id sq, es-pred wf, es-loc-init, es-loc-pred, es-state wf, es-state-when wf, atom-free-es-state, es-loc wf, es-init wf, es-le wf, es-isrcv wf, inheres wf, es-valtype wf, es-val wf, es-causle-le, atom-free-es-valtype, es-le-iff, es-E wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf